(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "arithmetics/nat.ma".
include "basics/bool.ma".
include "basics/lists/list.ma".


inductive operator : Type[0] ≝
| par:operator
| copar: operator
| seq: operator
| neg: operator.

let rec sum s on s ≝
match s with [
nil ⇒ 0
| cons h tl ⇒ h+sum tl].


(*
inductive atoms : Type[0] ≝
| atom: nat → atoms
| coatom : nat→ atoms.

inductive struct: Type[0] ≝
| u: struct
| b_node: operator → list atoms → struct
| node: operator → list struct → struct.



let rec length_s (s:struct) on s≝
match s with [
  u ⇒ 0
| b_node op l ⇒ length atoms l
| node op l ⇒ 1+ sum (map ? ? length_s l)].

definition lis ≝ (atom 1)::(atom 2)::(coatom 2)::(nil atoms).

definition stru ≝ (node copar ((b_node par lis)::(b_node copar lis)::(nil struct))).

definition stru2 ≝ (node par ((b_node par lis)::(stru)::(nil struct))).
lemma prova :  length_s stru2=11. normalize //

*)
inductive  struct :Type[0] ≝
| un : struct
| atom : nat → struct
| node : operator → list struct → struct.


notation "❲x❳" with precedence 45
for @{(atom $x)::(nil struct)}.

notation "○"with precedence 45
for @{nil struct}.

notation "𝐚" with precedence 80 for @{❲1❳}.
notation "𝐛" with precedence 80 for @{❲2❳}.
notation "𝐜" with precedence 80 for @{❲3❳}.
notation "𝐝" with precedence 80 for @{❲4❳}.


(*
notation "hvbox(hd break , tl)"
  right associative with precedence 40  
  for @{'cons $hd $tl}.

notation "[x]" with precedence 75
for @{par ($x,unit) }.



notation "〈x〉" with precedence 75
for @{seq ($x,unit)}.

notation "❨x❩" with precedence 75
for @{copar ($x,unit)}.

notation "¬x" with precedence 76
for @{neg ($x,unit)}.
*)

(*
  let rec append_struct (s1: struct) (s2: struct) on s1 ≝ match s1 with
[ atom n ⇒ s1
| un ⇒ s1
| node op l ⇒ node op (append ? l (s2::○))].


let rec estrai_list (l:list struct) n on n ≝
 match n with [
  O ⇒ (hd struct l (un))
  | S x ⇒ estrai_list (tail struct l) (x)].
  

let rec estrai_struct (s1:struct) (n:nat) on s1 ≝
match s1 with [
atom n ⇒ s1
| un ⇒ s1
| node op l ⇒ (estrai_list l n)].*)

definition eqb_op ≝ λs1,s2. match s1 with[
par ⇒ match s2 with [ par ⇒ true | _ ⇒ false]
| copar ⇒ match s2 with [copar ⇒ true | _ ⇒ false ]
| seq ⇒ match s2 with [seq ⇒ true | _ ⇒ false]
| neg ⇒ match s2 with [neg ⇒ true | _ ⇒ false]].

definition same_op ≝λs1,s2:struct. match s1 with[
  node op l ⇒ match s2 with [ node op2 l2 ⇒ eqb_op op op2 | _ ⇒ false ]
| _ ⇒ false]. 


let rec length_s (s:struct )  ≝
match s with [
  node op l ⇒ (sum (map ? ? length_s l))
 | _ ⇒ 1    ].
 
 
 
 (*
 Si contano i node, si lancia la i_flat per ogni nodo (ricorsivamente),
 si prova a cancellarlo se il padre corrisponde.
 Se si cancella si chiama con lo stesso numero (ma la dimensione è diminuita), altrmenti
 lo si aumenta (diminuisce?).  -→ sfrutto il fatto che ogni nodo ha un solo padre, ma
  quando sono al figlio non riesco più ad agganciarmi al padre.
  
  Uso il padre e per avere un unico caso conto i figli (quando sono finiti cambio il numero di padre):
  
  Si contano i node e si lancia la i1_flat per ogni nodo (ricorsivamente),
  per ogni i1_flat si lancia (ricorsivamente) i2_flat con l'indice del figlio,
  se il filgio corrisponde si aggancia al padre (vantaggio: si sa anche dove agganciarlo)
  se non esiste il figlio si rilancia la i1_flat.
  
  
  *)
  
 
let rec count_node s on s ≝ 
 match s with [
    node op l ⇒ 1+(sum (map ? ? count_node l))
  | _ ⇒ 0].
  

let rec i2_flat s padre_n_neg figlio_n on padre_n_neg  ≝
match padre_n_neg with [
  0 ⇒ 
| S m ⇒ 
].  
  
    
let rec i_flat s op n on n ≝
match n with [
  0 ⇒ match s with [
        node op_child l  ⇒match eqb_op op op_child with[
                        true ⇒ 
                      | false⇒ ]
      |  _ ⇒ s
| S m ⇒ 
 ].

(*
for s:sub_l 
  if op(s)==op then append res (map flat subl(s))
               else res+=node op(s) (map flat subl(s))
   
 
 
 
 
 
 
 
let rec flat_struct  (op:operator) (res:list struct) (s:struct) on s ≝
 match s with [
   node sub_op sub_l ⇒ match eqb_op op sub_op with[
                        true ⇒ node sub_op (append ? res (map ? ? (flat_struct op sub_l ) sub_l))
                      | false⇒ s]
 | _ ⇒ s
].
 (*
let rec flat_struct_l (l:list struct) (op:operator) on l ≝
match l with [
  nil ⇒ nil struct
| cons h tl ⇒ match h with [
    node sub_op l ⇒ match (eqb_op sub_op op) with [
      true ⇒ append struct l (flat_struct_l  tl op)
     |false ⇒ cons struct h (flat_struct_l  tl op)
     ]
  |  _ ⇒ cons struct h (flat_struct_l   tl op)
  ]
].  
*)

  
(*definition flat_struct ≝  λs:struct. 
        fold struct (list struct) (append struct) (nil struct) 
        (same_op s) 
        (λs1:struct.(s1::○))
        (match s with [node op l ⇒ l | _ ⇒ s::○]).*)
        
 (*
let rec flat (to_scan:list struct) (op:operator) on to_scan ≝
match to_scan with [
  nil ⇒ (nil struct)
| (cons h tl) ⇒ 
        (match h with [
              un ⇒ append ? (flat tl op) (un::○)
            | atom n ⇒ append ? (flat tl op) ((atom n)::○)
            | node subop subl ⇒ (match (eqb_s subop op) with [
                              true ⇒ (match subl with [
                                   nil ⇒ flat tl op
                                 | cons subh subtl ⇒ append ? 
                                      (append ? (flat subtl op) (subh::○)) (flat tl op)])

                            | false ⇒ append ? (flat tl op) ((node subop subl)::○)
                            ])
            ])
]. *)
(*
let rec flat (to_scan:list struct) (flattened:list struct) (op: operator)  on to_scan≝
match to_scan with[
nil ⇒ flattened
| (cons h tl) ⇒ 
    match h with[
      un ⇒ flat (tl) (append ? flattened (un::○)) op
      | (atom n) ⇒ flat (tl) (append ? flattened (atom n::○)) op
      | (node subop subl) ⇒  match (eqb_s op subop) with [
                              true ⇒ flat (tl) (append ? flattened (flat subl (nil struct) op)) op
                              | false ⇒ flat tl (append ? flattened (h::○)) op
                              ] 
                              
    ]
].
*)


(*
let rec flat_struct (to_scan:struct) on to_scan≝
match to_scan with [
  node op l ⇒ match l with [
                nil ⇒ nil struct 
              | cons hd tl ⇒ match hd with [
                           node subop subl ⇒ 
                              match eqb_op op subop with [
                                true ⇒ append ? (flat_struct node op tl) (subl)
                              | false ⇒ append ? (flat_struct node op tl) (hd::○)]
                         | _ ⇒ append ? (flat_struct node op tl) (hd::○)]
               ]
| _ ⇒ to_scan ].
*)(*

let rec flat_struct_r (to_scan:list struct) (res:list struct) (op:operator) on to_scan ≝
match to_scan with [
  nil ⇒ node op res 
| cons hd tl ⇒  match hd with [
                    node subop subl ⇒ match eqb_op subop op with [
                                        true ⇒ flat_struct_r tl (append ? res ((flat_struct_r subl (○) op)::○)) op
                                      | false ⇒ flat_struct_r tl (append ? res (hd::○)) op
                                      ]
                  | _ ⇒ flat_struct_r tl (append ? res (hd::○)) op
                ]
].
*)
(*
definition flat_struct ≝λs:struct.
match s with [
  node op l ⇒ flat_struct_r l (○) op
| _ ⇒ s].*)


notation "x,y" with precedence 90
for @{append ? $x $y$}.


(*check (node copar (𝐚,(node copar 𝐜)::○,𝐜,𝐝)) *)

(* lemma prova: (length_s  (node copar ((node copar ((node copar 𝐜)::○,𝐝))::𝐚)))= ?. normalize  *)

lemma prova: (flat_struct copar (○) (node copar ((node copar ((node copar 𝐜)::○,𝐝))::𝐚)))= ?. normalize  

let rec elim_un (to_scan:struct) (res:struct) on to_scan ≝
match to_scan with [
❲n❳ ⇒ append ? res (❲n❳::○)
un ⇒ ○
node op l = match l with [ 
            cons h::tl ⇒ 
            ○ ⇒ ○
            ]
].









